
#include "plugin.hpp"
#include <boost/format.hpp>

using namespace ie;

plugin::conditional_unification_t::conditional_unification_t( ie::weighted_abduction_t& ie )
  : callback_t( ie ) {
  
  /* Compile regular expressions, please. */
  string_list_t sl_regex_cups = m_ie.m_p_kbp->get_regex_cups();
  foreach( string_list_t, iter_rc, sl_regex_cups ) m_regex_cups.push_back( kb::pps_template_t(*iter_rc) );

}

bool plugin::conditional_unification_t::is_conditioned_predicate( string_list_t *p_out, const string &predicate ) {

  static string_list_t _temp_str;
  m_ie.m_p_kbp->get_conditioned_property( NULL == p_out ? &_temp_str : p_out, predicate );

  /* Anything else? */
  ssl_dict_t::iterator iter_cache = m_regex_cache.find( predicate );
  if( m_regex_cache.end() != iter_cache ) { ( NULL == p_out ? &_temp_str : p_out )->insert( p_out->end(), iter_cache->second.begin(), iter_cache->second.end() ); }
  else {
    foreach( vector<kb::pps_template_t>, iter_ppst, m_regex_cups ) {
      if( iter_ppst->regex.FullMatch( predicate ) ) { ( NULL == p_out ? &_temp_str : p_out )->push_back( iter_ppst->property ); m_regex_cache[predicate].push_back( iter_ppst->property ); }
    }
  }

  return NULL == p_out ? _temp_str.size()>0 : p_out->size()>0;
  
}

bool plugin::conditional_unification_t::generate_constraint( cset_t *p_out_cons, unifier_operator_t &opr, string_list_t &sl_requirements, int target, bool f_check_mode ) {
  
  opr.is_postponed = true;

  WHISPER( 5, m_hypotheses[opr.h1].to_string() << " ~ " << m_hypotheses[opr.h2].to_string() << endl );
      
  /* Constrain the targets by the requirements. */
  logical_variable_t tv1 = m_hypotheses[opr.h1].arguments[target-1], tv2 = m_hypotheses[opr.h2].arguments[target-1];

  static char buffer[1024]; sprintf( buffer, "%lu/%lu", tv1<tv2?tv1:tv2, tv1<tv2?tv2:tv1 );
      
  string_list_t sl_vars;
  bool          f_different_property = false;
  static int    req_id = 0;
      
  foreachc( string_list_t, iter_req, sl_requirements ) {
    
    string              req  = trim_copy( *iter_req );
    logical_variable_t  v1, v2;
    int                 req_type = 0;
    string              u_except;

    if( string::npos != req.find( ":" ) ) { req_type = 0;

      /* The nightmare starts. */
      string_list_t sl_req; split( sl_req, req, is_any_of(":") );
      var_hypo_dict_t::iterator v2h1 = m_ie.m_v2h.find( m_hypotheses[opr.h1].arguments[target-1] ),
        v2h2 = m_ie.m_v2h.find( m_hypotheses[opr.h2].arguments[target-1] );
      int           arg = lexical_cast<int>( sl_req[1] )-1;

      /* Any hits? */
      sil_dict_t::iterator iter_h1  = v2h1->second.find( sl_req[0] ),
        iter_h2  = v2h2->second.find( sl_req[0] );

      /* Choose one in the same group. */
      int lsg1 = -1, lsg2 = -1;

      if( v2h1->second.end() != iter_h1 ) {
        foreach(int_list_t, iter_rh, iter_h1->second) {
          WHISPER( 5, "V1:" << m_hypotheses[ *iter_rh ].to_string() << endl );
          if( m_hypotheses[opr.h1].group_id == m_hypotheses[ *iter_rh ].group_id ) { lsg1 = *iter_rh; break; }
        }
      }

      if( v2h2->second.end() != iter_h2 ) {
        foreach(int_list_t, iter_rh, iter_h2->second) {
          WHISPER( 5, "V2:" << m_hypotheses[ *iter_rh ].to_string() << endl );
          if( m_hypotheses[opr.h2].group_id == m_hypotheses[ *iter_rh ].group_id ) { lsg2 = *iter_rh; break; }
        }
      }
          
      if( v2h1->second.end() == iter_h1 || v2h2->second.end() == iter_h2 ) {

        /* Unbound. */
        if( m_ie.m_f_bc_from_same_prefix && (-1 != lsg1 || -1 != lsg2) ) {
              
          /* ! */
          if( -1 != lsg1 ) {
            if( 'h' == g_vm.p2v( m_hypotheses[ lsg1 ].arguments[0] )[0] ) { m_ilp_solver.fix_variable( opr.var_operator, 0.0 ); }
          }
              
          if( -1 != lsg2 ) {
            if( 'h' == g_vm.p2v( m_hypotheses[ lsg2 ].arguments[0] )[0] ) { m_ilp_solver.fix_variable( opr.var_operator, 0.0 ); }
          }
              
        }
            
        continue;
            
      }
          
      if( -1 == lsg1 || -1 == lsg2 ) { WHISPER( 5, "Ooops!" << endl ); continue; }
          
      v1 = m_hypotheses[ lsg1 ].arguments[arg];
      v2 = m_hypotheses[ lsg2 ].arguments[arg];
      u_except = sl_req[0];
          
      WHISPER( 5, "- requires unification of " << g_vm.p2v(v1) << " & " << g_vm.p2v(v2) << endl );
          
    } else { req_type = 1;
      int ireq = lexical_cast<int>( req );
      v1 = m_hypotheses[ opr.h1 ].arguments[ireq-1];
      v2 = m_hypotheses[ opr.h2 ].arguments[ireq-1];
      u_except = m_hypotheses[ opr.h1 ].to_string( PredicateArity );
    }

    WHISPER( 5, "- " << g_vm.p2v(v1) << " ~ " << g_vm.p2v(v2) << endl );
    
    if( v1 == v2 ) { continue; }
    if( v1 == tv1 && v2 == tv2 ) continue;

    /* Find u variable that causes unification of required
       variables, of course, except me. */
    int_list_t          &unifiers = m_ie.get_eu_dict( v1, v2 );
    ilp::variable_set_t local_requirements;
    bool                f_satisfied = false;
    
    foreach( int_list_t, iter_u, unifiers ) {
      unifier_t *p_unifier = m_ie.get_variable_cluster().get_unifier( *iter_u );
      if( p_unifier->var_operator == opr.var_operator ) continue;
      if( u_except == m_hypotheses[ p_unifier->p_operator->h1 ].to_string( PredicateArity ) ) continue;
      
      local_requirements.insert( p_unifier->var_operator );

      WHISPER( 5, "- Req: " << m_hypotheses[ p_unifier->p_operator->h1 ].to_string() << " ~ " << m_hypotheses[ p_unifier->p_operator->h2 ].to_string() << endl );
      
      if( f_check_mode ) {
        if( m_ilp_solver.get_variable_val( p_unifier->var_operator ) > 0.5 ) f_satisfied = true;
      }
    }

    if( 0 != local_requirements.size() ) {
      
      if( !f_check_mode )   (*p_out_cons)[ opr.var_operator ][ req_id++ ].insert( local_requirements.begin(), local_requirements.end() );
    else if( !f_satisfied ) return false;
      
    } else {
      
      /* Check v1 or v2 are bound or not. */
      var_hypo_dict_t::iterator v2h1 = m_ie.m_v2h_o.find( v1 ), v2h2 = m_ie.m_v2h_o.find( v2 );
      bool f_bound1 = false, f_bound2 = false;
      int  hb1 = -1, hb2 = -1;

      if( m_ie.m_v2h_o.end() != v2h1 ) {
        foreach( sil_dict_t, iter_h1list, v2h1->second ) {
          foreach( int_list_t, iter_h1, iter_h1list->second ) {
            if( opr.h1 != *iter_h1 ) { hb1 = *iter_h1; f_bound1 = true; break; }
          } }
      }
      
      if( m_ie.m_v2h_o.end() != v2h2 ) {
        foreach( sil_dict_t, iter_h2list, v2h2->second ) {
          foreach( int_list_t, iter_h2, iter_h2list->second ) {
            if( opr.h2 != *iter_h2 ) { hb2 = *iter_h2; f_bound2 = true; break; }
          } }
      }

      /* For textual entailment prediction. */
      if( m_ie.m_f_bc_from_same_prefix && 1 == req_type ) {
        
        if( (!f_bound1 || !f_bound2) ) {
          
          /* Make sure that v1 is not bound by H. */
          if( f_bound1 && !f_bound2 ) {
            if( 'h' == g_vm.p2v( m_hypotheses[ hb1 ].arguments[0] )[0] ) { f_bound2 = true; }
          }
            
          if( !f_bound1 && f_bound2 ) {
            if( 'h' == g_vm.p2v( m_hypotheses[ hb2 ].arguments[0] )[0] ) { f_bound1 = true; }
          }
            
        }
          
      }
          
      if( !f_bound1 || !f_bound2 ) {
        /* One of them are unbound, so we can continue. */
        WHISPER( 5, "- Unbound argument: " << g_vm.p2v(v1) << " or " << g_vm.p2v(v2) << endl );
        continue;
      }

      /* Let unification won't happen because both are bound by
         other properties. */
      if( f_check_mode ) return false;
      
      f_different_property = true;
      m_ilp_solver.fix_variable( opr.var_operator, 0.0 );
      break;

    }
        
    static char buffer[1024]; sprintf( buffer, "%lu/%lu", v1<v2?v1:v2, v1<v2?v2:v1 );
    sl_vars.push_back( string(buffer) );
        
  }

  if( f_different_property ) return false;

  return true;
  
}

bool plugin::conditional_unification_t::process() {

  WHISPER( 1, "plugin::conditional_unification_t::process()..." << endl );
  WHISPER( 1, "" ); g_progress_bar.wakeup( m_ie.m_unifiable.size() );

  cset_t u_cons;

  foreachc( unifiable_dict_t, iter_unisets, m_ie.m_unifiable ) {
    g_progress_bar.goto_school();

    /* How are you? */
    string_list_t conditioned_property;
    if( !is_conditioned_predicate( &conditioned_property, iter_unisets->first ) ) continue;

    foreach( string_list_t, iter_cp, conditioned_property ) {
      WHISPER( 3, iter_unisets->first << " ... " << *iter_cp << endl );

      /* Process the property. */
      static pcrecpp::RE regex_split( ".*?/\\d+:(\\d+)" ), regex_tr( " ~ (.*)" );
      string requirements; string_list_t sl_requirements;
      int    target;
      regex_split.PartialMatch( *iter_cp, &target );
      regex_tr.PartialMatch(    *iter_cp, &requirements );
      split( sl_requirements, requirements, is_any_of(",") );
    
      foreachc( vector<unifier_operator_t*>, iter_opr, iter_unisets->second ) {

        if( m_ie.is_timeout() ) return false;

        generate_constraint( &u_cons, *(*iter_opr), sl_requirements, target );

      }
    }
    
  }

  /* Remove interdependent variables! */
  foreach( cset_t, iter_ua, u_cons ) {
    for( unordered_map<int, ilp::variable_set_t>::iterator iter_vvs = iter_ua->second.begin(); iter_ua->second.end() != iter_vvs; ++iter_vvs ) {
      vector<ilp::variable_t> to_be_erased;
      foreach( ilp::variable_set_t, iter_v, iter_vvs->second ) {
        cset_t::iterator iter_dependents = u_cons.find( *iter_v );
        if( u_cons.end() == iter_dependents ) continue;
      
        for( unordered_map<int, ilp::variable_set_t>::iterator iter_dependent = iter_dependents->second.begin(); iter_dependents->second.end() != iter_dependent; ++iter_dependent ) {
          ilp::variable_set_t::iterator iter_circular = iter_dependent->second.find( iter_ua->first );
          if( iter_dependent->second.end() != iter_circular ) {
            /* Identified u1 <= u2 + u3, u2 <= u1 + u4. Delete both variables in the RHS. */
            iter_dependent->second.erase( iter_circular );
            to_be_erased.push_back( *iter_v );
          }
        }
      }
      foreach( vector<ilp::variable_t>, iter_tbe, to_be_erased ) {
        iter_vvs->second.erase( *iter_tbe );
      }
    }
  }
  
  /* Actually create the constraints. */
  foreach( cset_t, iter_ua, u_cons ) {
    for( unordered_map<int, ilp::variable_set_t>::iterator iter_vvs = iter_ua->second.begin(); iter_ua->second.end() != iter_vvs; ++iter_vvs ) {
      ilp::constraint_template_t *p_cargs;
      m_ilp_solver.add_constraint( &p_cargs );
      p_cargs->set( 0, ilp::CT_NO_MATTER );
      p_cargs->push_back( iter_ua->first, -1.0 );
      p_cargs->push_back( iter_vvs->second, 1.0 );
    }
  }
  
  g_progress_bar.goto_hell();

  /* @CONSTR: e_{x,y} <= u_1 + u_2 + ... u_i */
        /* We still need to guarantee that unification of these two literals does not suggest depended variables. */
//         bool f_skip = false;
//         foreach( vector<ilp::constraint_t>, iter_c, cons_dep ) {
//           ilp::constraint_template_t *p_con  = m_ilp_solver.get_constraint( *iter_c );
//           f_skip = true;
//           foreach( int_list_t, iter_u, p_unifier->p_operator->unifiers ) {
//             unifier_t          *p_unifier = m_vc.get_unifier( *iter_u );
//             ilp::variable_t    var_e     = m_ie.find_variable_e( p_unifier->v1, p_unifier->v2, 0 );
//             if( p_con->variables.end() == find( p_con->variables.begin(), p_con->variables.end(), var_e ) ) { f_skip = false; break; }
//           }
//           if( f_skip ) break;
//         }

//         if( f_skip ) continue;

//         p_clonely->push_back( p_unifier->var_operator, 1.0 );
//         sl_uset.push_back( m_hypotheses[ p_unifier->p_operator->h1 ].to_string() + "=" + m_hypotheses[ p_unifier->p_operator->h2 ].to_string() );

//     m_ie.m_constraints.insert( g_vm.p2v(v1) + "=" + g_vm.p2v(v2) + " => " + (0 == sl_uset.size() ? "_|_" : join( sl_uset, " v " )) );

//   }
  
  return true;
  
}

bool plugin::xor_constraint_t::process() {

  WHISPER( 1, "plugin::xor_constraint_t::process()..." << endl );
  
  iil_dict_t disjoint_set;
  
  foreach( literal_vector_t, iter_h, m_hypotheses ) {

    if( iter_h->is_discarded ) continue;

    int_list_t il_djid;
    if( m_ie.m_p_kbp->get_disjoint_id( &il_djid, iter_h->to_string( PredicateArity ) ) ) {
      foreach( int_list_t, iter_djid, il_djid )
        disjoint_set[ *iter_djid ].push_back( iter_h->id );
    }
    
    iiset_dict_t mx_set;
    ii_dict_t    g2h;
    
    foreach( int_set_t, iter_c, iter_h->children ) {
      if( m_hypotheses[ *iter_c ].is_discarded ) continue;
      mx_set[ m_hypotheses[ *iter_c ].xor_id ].insert( m_hypotheses[ *iter_c ].group_id );
      g2h[ m_hypotheses[ *iter_c ].group_id ] = *iter_c;
    }
    
    foreach( iiset_dict_t, iter_mx, mx_set ) {

      if( !m_ie.m_f_expl_mutual_exclusive && -1 == iter_mx->first ) continue;
      if( 1 >= iter_mx->second.size() ) continue;

      ilp::constraint_template_t *p_cxor;
      m_ilp_solver.add_sos1( &p_cxor );
      //m_ilp_solver.add_constraint( &p_cxor );
      p_cxor->set( ilp::CT_NO_MATTER, 1 );

      WHISPER( 3, "XOR [" << iter_mx->first << "]: " );
    
      foreach( int_set_t, iter_hmx, iter_mx->second ) {
        //p_cxor->push_back( m_hypotheses[ g2h[ *iter_hmx ] ].var_pay, m_hypotheses[ g2h[ *iter_hmx ] ].number );
        p_cxor->push_back( m_hypotheses[ g2h[ *iter_hmx ] ].var_pay, 1.0 );
        SWHISPER( 3, m_hypotheses[ g2h[ *iter_hmx ] ].to_string() << ", " );
      }

      SWHISPER( 3, ":)" << endl );
    }
    
  }

  /* Impose constraints on the disjoint set. */
  foreach( iil_dict_t, iter_pc, disjoint_set ) {

    string_list_t sl_target;
    string        prop = m_ie.m_p_kbp->get_disjoint_prop( iter_pc->first );
    split( sl_target, prop, is_any_of("^") );
    
    /* Make them pairwise because set_disjoint(a/1, b/1, c/1) implies
       a(x) => !b(x) ^ !c(x), b(x) => !a(x) ^ !c(x), c(x) => !a(x) ^ !b(x). */
    foreach( int_list_t, iter_h1, iter_pc->second ) {
      for( int_list_t::iterator iter_h2 = next( iter_h1 ); iter_pc->second.end() != iter_h2; ++iter_h2 ) {
        
        literal_t &h1 = m_hypotheses[ *iter_h1 ], &h2 = m_hypotheses[ *iter_h2 ];
        ilp::variable_set_t e_set;
        int                 rhs = 1;

        if( h1.predicate == h2.predicate ) continue;
        
        foreach( string_list_t, iter_arg, sl_target ) {

          int i = lexical_cast<int>( *iter_arg ) - 1;
          
          /* Are they unifiable? */
          if( h1.arguments[i] == h2.arguments[i] ) continue;
          vi_dict_t::iterator iter_v1 = m_ie.m_var_vc.find( h1.arguments[i] ), iter_v2 = m_ie.m_var_vc.find( h2.arguments[i] );
          if( m_ie.m_var_vc.end() == iter_v1 || m_ie.m_var_vc.end() == iter_v2 || ((m_ie.m_var_vc.end() != iter_v1 && m_ie.m_var_vc.end() != iter_v2) && iter_v1->second != iter_v2->second) ) { e_set.clear(); break; }

          for( int t=0; t<m_ie.m_var_cx[ h1.arguments[i] ].size(); t++ )
            e_set.insert( m_ie.add_variable_e( h1.arguments[i], ilp::INVALID_HANDLE, h2.arguments[i], ilp::INVALID_HANDLE, t ) );

          rhs++;
          
        }

        if( 0 == e_set.size() ) continue;

        ilp::constraint_template_t *p_cdj;
        m_ilp_solver.add_constraint( &p_cdj );
        p_cdj->set( ilp::CT_NO_MATTER, rhs );

        p_cdj->push_back( h1.var_pay, 1.0 );
        p_cdj->push_back( e_set, 1.0 );
        p_cdj->push_back( h2.var_pay, 1.0 );
        
      }
    }
    
  }
  
  return true;
  
}

bool plugin::prohibit_same_multiple_explanations_t::process() {

  WHISPER( 1, "plugin::prohibit_same_multiple_explanations_t::process() ..." << endl );

  string_set_t ignore_ms = m_ie.m_p_kbp->get_ignore_ms();
  
  foreachc( slpl_dict_t, iter_sets, m_ie.m_pa2h ) {

    if( 1 == iter_sets->second.size() ) continue;
    if( has_key( ignore_ms, iter_sets->first ) ) continue;

    unordered_map<int, ilp::variable_set_t> h_set;
    
    foreachc( int_list_t, iter_h1, iter_sets->second ) {
      for( int_list_t::const_iterator iter_h2 = next( iter_h1 ); iter_sets->second.end() != iter_h2; ++iter_h2 ) {
        
        if( m_ie.is_timeout() ) return false;

        /* Check their ancestor. */
        int common_ancestor = m_hypotheses.size()+1;
        
        foreach( int_set_t, iter_a1, m_hypotheses[*iter_h1].ancestor ) {
          foreach( int_set_t, iter_a2, m_hypotheses[*iter_h2].ancestor ) {
            if( *iter_a1 == *iter_a2 && common_ancestor > *iter_a1 ) common_ancestor = *iter_a1;
          } }

        if( m_hypotheses.size()+1 == common_ancestor ) continue;

        h_set[ common_ancestor ].insert( m_hypotheses[*iter_h1].var_pay );
        h_set[ common_ancestor ].insert( m_hypotheses[*iter_h2].var_pay );

        /* The unification won't happen. */
        unifier_operator_t *p_u = m_ie.get_unifier_op( *iter_h1, *iter_h2 );
        if( NULL != p_u ) m_ilp_solver.fix_variable( p_u->var_operator, 0.0 );
            
      } }
    
    /* OK, hmm... */
    for( unordered_map<int, ilp::variable_set_t>::iterator iter_hs=h_set.begin(); h_set.end()!=iter_hs; ++iter_hs ) {
      ilp::constraint_template_t *p_cxor;
      m_ilp_solver.add_sos1( &p_cxor );
      p_cxor->push_back( iter_hs->second, 1.0 );
    }
    
  }

  return true;
  
}

void _harvest_children( int_set_t *p_out, literal_t &lt, literal_vector_t &hypotheses ) {
  foreach( int_set_t, iter_s, lt.sibling )  p_out->insert( *iter_s );
  foreach( int_set_t, iter_c, lt.children ) _harvest_children( p_out, hypotheses[ *iter_c ], hypotheses );
}

void plugin::prohibit_circular_zero_t::_apply_circular_zero_blocking( int_set_t &expl, int_set_t &conseq, ilp::variable_t var_unifier_operator, literal_t &h ) {
  
  /* Retrieve all the unification between explanation and consequent. */
  ilp::variable_set_t u_set;
  foreach( int_set_t, iter_expl, expl ) {
    foreach( int_set_t, iter_conseq, conseq ) {
      unifier_operator_t *p_opr = m_ie.get_unifier_op( *iter_expl, *iter_conseq );
      if( NULL == p_opr ) continue;
      u_set.insert( p_opr->var_operator );
    } }

  if( 0 == u_set.size() ) return;
      
  ilp::constraint_template_t *p_con;
  m_ilp_solver.add_constraint( &p_con );
  p_con->set( -2.0*u_set.size(), ilp::CT_NO_MATTER, 2, var_unifier_operator, -1.0*u_set.size(), h.var_reduce, -1.0*u_set.size() );
  p_con->push_back( u_set, -1.0 );
  
}

bool plugin::prohibit_circular_zero_t::process() {

  WHISPER( 1, "plugin::prohibit_circular_zero_t::process() ..." << endl );
  
  foreachc( unifiable_dict_t, iter_sets, m_ie.m_unifiable ) {
    foreachc( vector<unifier_operator_t*>, iter_opr, iter_sets->second ) {

      if( m_ie.is_timeout() ) return false;
      
      /* Retrieve their explanations and consequents. */
      int_set_t expl1, expl2, conseq1, conseq2;
      literal_t &h1 = m_hypotheses[ (*iter_opr)->h1 ], &h2 = m_hypotheses[ (*iter_opr)->h2 ];
      
      _harvest_children( &expl1, h1, m_hypotheses );
      _harvest_children( &expl2, h2, m_hypotheses );
      
      conseq1.insert( h1.ancestor.begin(), h1.ancestor.end() );
      conseq2.insert( h2.ancestor.begin(), h2.ancestor.end() );

      _apply_circular_zero_blocking( expl1, conseq2, (*iter_opr)->var_operator, h1 );
      _apply_circular_zero_blocking( expl2, conseq1, (*iter_opr)->var_operator, h2 );
      
    }
  }
  
  return true;
}
